\section{Fixed Point Logics}
\subsection{Expressiveness}
\begin{frame}
  \frametitle{Expressiveness}
\bi
\item Most logics cannot express many tractable graph properties: graph connectivity, reachability.
\item They lack mechanisms for expressing fixed point computations.
\item Ex: the transitive closure query.
\smallskip

Given a binary relation $R$, we can express $R^0,R^1,\dots,$ where $(a,b) \in R^i$ means there is a path from $a$ to $b$ of length at most $i$. The transitive closure of $R$ is
\[ R^\infty=\bigcup_{i=0}^\infty R^i \]
\item We study logics extended with operators for computing fixed points of various operators. 
\ei
\end{frame}
%\subsection{Outline}
%\begin{frame}
% \frametitle{Outline}
%\bi
%\item Basics of fixed point theory
%\item Various extensions of FO with fixed point operators
%\item Show how to extend FO with an operator for computing the transitive closure
%\ei
%\end{frame}
\subsection{Least Fixed Point}
\begin{frame}
  \frametitle{Least Fixed Point}
Consider a partially ordered (finite) set $\langle U, \prec \rangle$. Given a set $U$, an \ii{operator} on $U$ is a mapping $F: \wp(U) \rightarrow \wp(U)$. 
\medskip

An operator $F$ is 
\bi
\item ~\ii{monotone} if $X \subseteq Y$ implies $F(X) \subseteq F(Y)$
\item and \ii{inflationary} if $X \subseteq F(X)$ 
\ei
for all $X \in \wp(U)$.
\medskip

Given an operator $F: \wp(U) \rightarrow \wp(U)$, a set $X \subseteq U$ is a \ii{fixed point} of $F$  if $F(X)=X$. A set $X \subseteq U$ is a \defn{least fixed point} of $F$, if it is a fixed point, and for every other fixed point $Y$ of $F$ we have $X \subseteq Y$.


\end{frame}
\begin{frame}
  \frametitle{Least Fixed Point}
Consider the sequence:
\beq
X^0 = \emptyset, X^{i+1} = F(X^i)
\eeq{eqn:seq}
\bi
\item $F$ is \ii{inductive} if the sequence \eqref{eqn:seq} is increasing: $X^i \subseteq X^{i+1}$ for all $i$.

\item Every monotone operator $F$ is inductive.


\item If $F$ is inductive, we define
\beeq
X^\infty=\bigcup_{i=0}^\infty X^i
\eeeq

Since $U$ is finite, there is a number $n$ such that $X^\infty=X^n$.
\ei

\end{frame}
\subsection{An Example}
\begin{frame}
\frametitle{An Example}

Let $E$ be a binary relation on a finite set $A$, and let $F: \wp(A^2)\rightarrow \wp(A^2)$ be the operator defined by \defn{$F(X)=E \cup (E \circ X)$}
 
$E \circ X=\{ (a,b) \mid (a,c) \in E, (c,b) \in X, \hbox{ for some } c \in A\}$

\bi
\item This operator is monotone: if $X \subseteq Y$, then $E \circ X\subseteq E\circ Y$.
\item Let us define the sequence $X^i,i\geq 0$.
\beeq \ba l
X^0=\emptyset\\
X^1=E \cup (E \circ \emptyset)=E\\
X^2=E \cup (E \circ E)=E \cup E^2\\
\cdots\\
X^i=E \cup \dots \cup E^i
\ea \eeeq
i.e. the set of pairs connected by paths of length at most $i$
\item The sequence reaches a fixed point $X^\infty$, which is the transitive closure of $E$.
\ei

\end{frame}
\subsection{Theorem (Tarski-Knaster)}
\begin{frame}
\frametitle{Theorem (Tarski-Knaster)}

Every \underline{monotone} operator $F: \wp(U) \rightarrow \wp(U)$ has a least fixed point $\bb{lfp}(F)$, which can be defined as
$$\bb{lfp}(F) = \bigcap\{X \mid X=F(X)\}.$$
Furthermore, $\bb{lfp}(F)= X^\infty = \bigcup_i X^i$, for the sequence $X^i$ defined by
$$
X^0 = \emptyset, X^{i+1} = F(X^i)
$$
% \eqref{eqn:seq}.
\medskip

\end{frame}
\subsection{Inflationary Fixed Point}
\begin{frame}
\frametitle{Inflationary Fixed Point} 

\bi
\item $F$ is inflationary; $X\subseteq F(X)$ for all $X$ \\$\Rightarrow$ $F$ is inductive; the sequence \eqref{eqn:seq} is increasing and reaches a fixed point $X^\infty$.
\ei
\bigskip
\pause

Now, suppose $F$ is an arbitrary operator. We associate an inflationary operator $F_{infl}$ defined by $F_{infl}(X)=X\cup F(X)$. Then $X^\infty$ for $F_{infl}$ is called the \defn{inflationary fixed point} of $F$.
$$\bb{ifp}(F)=\bigcup_i X^i, \hbox{ where } X^0=\emptyset \mbox{ and } X^{i+1}=X^i\cup F(X^i)$$


\end{frame}
\subsection{Partial Fixed Point}
\begin{frame}
\frametitle{Partial Fixed Point} 

Consider an arbitrary operator $F: \wp(U) \rightarrow \wp(U)$ and the sequence \eqref{eqn:seq}. This sequence does not need to be inductive. The \defn{partial fixed point} of $F$ is 
\beeq 
\bb{pfp}(F)= \left\{
\ba {lcl}
X^n & \hbox{ if } & X^n=X^{n+1}\\
\emptyset &\hbox{ if } & X^n \neq X^{n+1} \hbox{ for all } n\leq 2^{|U|} 
\ea \right.
\eeeq
\smallskip

\pause
\begin{prop}
If $F$ is monotone, then $\bb{lfp}(F)=\bb{ifp}(F)=\bb{pfp}(F).$
\end{prop}
\end{frame}

\subsection{FO with Fixed Point Operators}
\begin{frame}
\frametitle{FO with Fixed Point Operators}

Suppose we have a relational vocabulary $\sigma$, and an additional relation symbol $R \notin \sigma$ of arity $k$.
Let $\varphi(R,x_1,\dots,x_k)$ be a formula of vocabulary $\sigma \cup \{R\}$. 
\medskip

For each $\mathfrak{A} \in \textup{STRUCT}[\sigma]$, the formula $\varphi(R,\vec{x})$ gives rise to an operator $F_\varphi : \wp(A^k)\rightarrow \wp(A^k)$ defined as:

\begin{displaymath}
  \begin{array}{rcl}
    F_\varphi(X) &= &\{\vec{a} \mid \mathfrak{A} \models \varphi(X/R,\vec{a})\} \\
    & = & \{\vec{a} \mid \mathfrak{A'} \models \varphi(\vec{a})\},
  \end{array}
\end{displaymath}
%$$F_\varphi(X)=\{\vec{a} \mid \mathfrak{A} \models \varphi(X/R,\vec{a})\}$$

%where $\varphi(X/R,\vec{a})$ means that $R$ is interpreted as $X$ in $\varphi$; if
where $\mathfrak{A}'$ is a $(\sigma \cup \{R\})$-structure expanding $\mathfrak{A}$, in which relation symbol $R$ is interpreted as the vectors of terms in $X$.%, then $ \mathfrak{A}' \models \varphi'(\vec{a})$.
\medskip
\pause

\bi
\item The idea of fixed point logics is to add formulae for computing fixed points of operators $F_\varphi$.
\ei
\end{frame}

\subsection{The Logics IFP}
\begin{frame}
\frametitle{The Logics IFP}

If $\varphi(R,\vec{x})$ is a formula, where $R$ is a $k$-ary, and $\vec{t}$ is a tuple of terms, where $|\vec{x}|=|\vec{t}|=k$, then
$$[\bb{ifp}_{R,\vec{x}}\varphi(R,\vec{x})](\vec{t})$$
is a formula, whose free variables are those of $\vec{t}$, with the semantics:
$$\mathfrak{A} \models [\bb{ifp}_{R,\vec{x}}\varphi(R,\vec{x})](\vec{a}) \hbox{ iff } \vec{a} \in \bb{ifp}(F_\varphi)$$


\end{frame}
%\begin{frame}
%    $\fA \models [ifp \phi(X,\vec{x})](\vec{a})$, since
%    $\vec{a} \in ifp(F_\phi)$, where
%\bi
%    \item X is the transitive closure relation of E (the initial edges)
%    \item $\vec{x}$ is any binary vector (representing an edge)
%    \item $\vec{a}$ is any specific pair of nodes of the same clique
%    \item $F_\phi$ should be displayed in detail based on the example. why?
%      because i am again confused at this point although i pay
%      attention to detail. ;-)
%\ei
% \end{frame}
\subsection{The Logics PFP}
\begin{frame}
\frametitle{The Logics PFP}

If $\varphi(R,\vec{x})$ is a formula, where $R$ is a $k$-ary, and $\vec{t}$ is a tuple of terms, where $|\vec{x}|=|\vec{t}|=k$, then
$$[\bb{pfp}_{R,\vec{x}}\varphi(R,\vec{x})](\vec{t})$$
is a formula, whose free variables are those of $\vec{t}$, with the semantics:
$$\mathfrak{A} \models [\bb{pfp}_{R,\vec{x}}\varphi(R,\vec{x})](\vec{a}) \hbox{ iff } \vec{a} \in \bb{pfp}(F_\varphi)$$


\end{frame}
\subsection{The Logics LFP}
\begin{frame}
\frametitle{The Logics LFP}

\bi
\item Least fixed points are guaranteed to exist only for monotone operators. 
\ei
\pause

\begin{lemma}
Testing if $F_\varphi$ is monotone is undecidable for FO formulae $\varphi$.
\end{lemma}

\pause
\bi
\item We impose some syntactic restrictions such as \ii{positive} (resp. \ii{negative}) occurence of a relation $R$ in a given formula $\varphi$.

\item Ex: $\exists x \neg R(x) \vee \neg \forall y \forall z \neg (R(y) \wedge \neg R(z))$

\pause
\item A formula is \ii{positive in $R$} if there are no negative occurrences of $R$ in it; either all occurrences of $R$ are positive, or there are none at all.
\ei
\end{frame}
\begin{frame}
\frametitle{The Logics LFP}

If $\varphi(R,\vec{x})$ is a formula positive in $R$, where $R$ is a $k$-ary, ant $\vec{t}$ is a tuple of terms, where $|\vec{x}|=|\vec{t}|=k$, then
$$[\bb{lfp}_{R,\vec{x}}\varphi(R,\vec{x})](\vec{t})$$
is a formula, whose free variables are those of $\vec{t}$, with the semantics:
$$\mathfrak{A} \models [\bb{lfp}_{R,\vec{x}}\varphi(R,\vec{x})](\vec{a}) \hbox{ iff } \vec{a} \in \bb{lfp}(F_\varphi)$$

\pause
\begin{lemma}
  If $\varphi(R,\vec{x})$ is positive in $R$, then $F_\varphi$ is monotone.
\end{lemma}

\end{frame}
\subsection{Examples}
\begin{frame}
\frametitle{Examples}
\framesubtitle{Transitive Closure}

Let $E$ be a binary relation, and let $\varphi(R,x,y)$ be
$$E(x,y) \vee \exists z (E(x,z) \wedge R(z,y))$$
This is positive in $R$. Let $\psi (u,v) = [\bb{lfp}_{R,x,y}\varphi(R,x,y)](u,v)$. What does this formula define?
\medskip

\pause
\bi
\item Consider the operator $F_\varphi$. For a set $X$, $F_\varphi(X)=E\cup (E \circ X)$. 
\pause
\item This operator's least fixed point is the transitive closure of $E$.
\pause
\item Hence, $\psi (u,v)$ defines the transitive closure of $E$. The graph connectivity is LFP-definable by the sentence $\forall u \forall v ~ \psi(u,v).$
\ei
\end{frame}

%\begin{frame}
%\frametitle{Examples}
%\framesubtitle{Acyclicity}
%
%Consider graphs whose edge relation is $E$, and the formula $\alpha (S,x)$ given by
%$$\forall y (E(y,x) \rightarrow S(y)) $$
%
%\begin{overprint}
%
%\onslide<1>
%
%This is positive in $S$. The operator $F_\alpha$  takes a set $X$ and returns the set of all nodes $x$ such that all the nodes $y$ from which there is an edge to $x$ are in $X$.
%Iterating the operator:
%\bi
%\item $F_\alpha(\emptyset)$ is the set of nodes of in-degree 0.
%\item $F_\alpha(F_\alpha(\emptyset))$ is the set of nodes $a$ such that all nodes $b$ with edges $(b,a)\in E$ have in-degree 0. i.e. the set of nodes $a$ such that all paths ending in $a$ have length at most 1.
%
%$\cdots$
%
%\item At the $i$th stage of the iteration we get the set of nodes $a$ such that all the paths ending in $a$ have length at most $i$.
%  \ei
%  
%\onslide<2>
%When we reach the fixed point, we have nodes such that all the paths ending in them are finite. Hence, the formula
%$$\forall u [\bb{lfp}_{S,x}\alpha(S,x)](u)$$
%tests if a graph is acyclic.  
%
%\end{overprint}
%
%\end{frame}

\begin{frame}
\frametitle{Examples}
 \framesubtitle{Arithmetic on Successor Structure}
 Consider the structures of vocabulary (\underline{min},\underline{succ}). The structures will be of the form $\langle \{0,\dots,n-1\},0,\{(i,i+1)\mid i+1 \leq n-1\}\rangle$.
\medskip
\bi
\item How to define
$$+=\{(i,j,k) \mid i+j=k\} \hbox{  and  } \times=\{(i,j,k) \mid i \cdot j =k\}$$
on such structures?
\medskip
\pause

\item {\sl Nested} least point operators
\ei 
\medskip

\end{frame}

\begin{frame}
\frametitle{Examples}
 \framesubtitle{Arithmetic on Successor Structure}
For $+$, we use the recursive definition:
\beeq \begin{split} 
x + 0 &= x\\
x + (y+1) &= (x+y)+1
\end{split} \eeeq

Let $R$ be ternary and $\beta_+(R,x,y,z)$ be
$$(y = \hbox{\underline{min}} \wedge z=x) \vee \exists u \exists v \big(R(x,u,v) \wedge \hbox{\underline{succ}}(u,y) \wedge \hbox{\underline{succ}}(v,z)\big)$$

This formula is positive in $R$ and
$$\varphi_+(x,y,z) = [\bb{lfp}_{R,x,y,z}\beta_+(R,x,y,z)](x,y,z)$$


\end{frame}

\begin{frame}
\frametitle{Examples}
 \framesubtitle{Arithmetic on Successor Structure}

Using $+$, we can define $\times$:
\beeq \begin{split} 
x \cdot 0 &= 0\\
x \cdot (y+1) &= (x \cdot y)+x
\end{split} \eeeq

Let $S$ be ternary and $\beta_\times(S,x,y,z)$ be
$$(y = \hbox{\underline{min}} \wedge z=\hbox{\underline{min}}) \vee \exists u \exists v \big(S(x,u,v) \wedge \underline{\text{succ}}(u,y) \wedge \varphi_+(x,v,z)\big)$$

This formula is positive in $S$ and
$$\varphi_\times(x,y,z) = [\bb{lfp}_{S,x,y,z}\beta_\times(S,x,y,z)](x,y,z)$$
\end{frame}

\subsection{$\lfpsimult$}
\begin{frame}
\frametitle{$\lfpsimult$}
\bi
\item We introduce  a tool of \defn{simultaneous fixed points}, which allows one to iterate several formulae at once.
\ei
\medskip

\pause
Let $\sigma$ be a relational vocabulary, and $R_1, \dots, R_n$ additional relation symbols, with $R_i$ being of arity $k_i$. Let $\vec{x}_i$ be a tuple of variables of length $k_i$. Consider a sequence $\Phi$ of formulae
\beq \ba c
\varphi_1(R_1,\dots,R_n,\vec{x}_1),\\
\cdots,\\
\varphi_n(R_1,\dots,R_n,\vec{x}_n),\\
\ea \eeq {eqn:family}
of vocabulary $\sigma \cup \{R_1,\dots,R_n\}$. Assume that all $\varphi_i$'s are positive in all $R_j$'s.

\end{frame}

\begin{frame}
\frametitle{$\lfpsimult$}


Then, for a $\sigma$-structure $\mathfrak{A}$, each $\varphi_i$ defines an operator
$$F_i : \wp(A^k_1) \times \dots \times \wp(A^k_n) \rightarrow \wp(A^k_i)$$
given by
$$F_i(X_1,\dots,X_n) = \{\vec{a}\in A^k_i \mid \mathfrak{A} \models \varphi_i(X_1/R_1,\dots,X_n/R_n,\vec{a})\}$$

We can combine these operators $F_i$'s into one operator
$$\vec{F}:\wp(A^k_1)\times\dots\times \wp(A^k_n)\rightarrow \wp(A^k_1)\times\dots\times \wp(A^k_n)$$
given by
$$\vec{F}(X_1,\dots,X_n) = (F_1(X_1,\dots,X_n),\dots,F_n(X_1,\dots,X_n))$$


\end{frame}


\begin{frame}
\frametitle{$\lfpsimult$}


A sequence of sets $(X_1,\dots,X_n)$ is a \ii{fixed point} of $\vec{F}$ if $\vec{F}(X_1,\dots,X_n)=(X_1,\dots,X_n)$. If for every fixed point $(Y_1,\dots,Y_n)$ we have $X_1 \subseteq Y_1,\dots,X_n\subseteq Y_n$, then it is the \defn{least fixed point} of $\vec{F}$.
\medskip
\pause
\bi
\item $\wp(A^k_1)\times \dots \times \wp(A^k_n)$ is partially ordered component-wise by $\subseteq$, and $\vec{F}$ is component-wise monotone. 
\item Hence it can be iterated:

\beeq \ba l
\vec{X}^0=(\emptyset,\dots,\emptyset)\\
\vec{X}^{i+1}=\vec{F}(\vec{X}^i)\\
\vec{X}^\infty = \bigcup_{i=1}^\infty \vec{X}^i = ( \bigcup_{i=1}^\infty \vec{X}_1^i, \dots,  \bigcup_{i=1}^\infty \vec{X}_n^i)
\ea \eeeq 

\item $\vec{X}^\infty=\bb{lfp}(\vec{F})$
\ei
\end{frame}

\begin{frame}
\frametitle{$\lfpsimult$}
If $\Phi$ is a family of formulae, and $\vec{t}$ is a tuple of terms of length $k_i$, then
$$[\bb{lfp}_{R_i,\Phi}](\vec{t})$$
is a formula with the semantics $\mathfrak{A}\models [\bb{lfp}_{R_i,\Phi}](\vec{a})$ iff $\vec{a}$ belongs to the $i$th component of $\vec{X}^\infty$.
\end{frame}


%%% Local Variables:
%%% fill-column: 72
%%% TeX-PDF-mode: t
%%% TeX-debug-bad-boxes: t
%%% TeX-master: "slides"
%%% TeX-parse-self: t
%%% TeX-auto-save: t
%%% reftex-plug-into-AUCTeX: t
%%% End:
